;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark -*-
;;; File: code-for-lists2.lisp
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations
;;; under the License.
;;;
;;; The Original Code is SNARK.
;;; The Initial Developer of the Original Code is SRI International.
;;; Portions created by the Initial Developer are Copyright (C) 1981-2006.
;;; All Rights Reserved.
;;;
;;; Contributor(s): Mark E. Stickel <stickel@ai.sri.com>.

(in-package :snark)

(defun declare-code-for-lists2 ()
  (declare-constant nil #| :constructor t :sort 'null |#)	;not sorted or a constructor unless user specifies but (/= nil ($$cons x y))
  (setf *cons* (declare-function '$$cons 2 :constructor t :to-lisp-code 'cons-term-to-lisp :sort 'cons))
  (declare-function '$$list :any :macro t :input-code 'input-lisp-list)
  (declare-function '$$list* :any :macro t :input-code 'input-lisp-list*)

  (declare-relation-rewriter1 '$$listp   1 'listp-atom-rewriter)
  (declare-relation-rewriter1 '$$consp   1 'consp-atom-rewriter)
  (declare-relation-rewriter1 '$$null    1 'null-atom-rewriter)

  (declare-function '$$car 1 :rewrite-code 'car-term-rewriter)
  (declare-function '$$cdr 1 :rewrite-code 'cdr-term-rewriter)

  (declare-function '$$append  2 :rewrite-code 'append-term-rewriter)

  (declare-relation-rewriter1 '$$member  2 'member-atom-rewriter :sort '((2 list)))
  )

(defun listp-atom-rewriter (atom subst) (characteristic-atom-rewriter atom subst #'listp 'listp))
(defun consp-atom-rewriter (atom subst) (characteristic-atom-rewriter atom subst #'consp 'consp))
(defun null-atom-rewriter  (atom subst) (characteristic-atom-rewriter atom subst #'null  'null))

(defun car-term-rewriter (term subst)
  (let ((x (first (args term))))
    (if (dereference x subst :if-compound-cons t)
        (carc x)
        none)))

(defun cdr-term-rewriter (term subst)
  (let ((x (first (args term))))
    (if (dereference x subst :if-compound-cons t)
        (cdrc x)
        none)))

(defun append-term-rewriter (term subst)
  (mvlet (((:list a b) (args term)))
    (if (and (not (eq none (setf a (true-list a subst))))
             (not (eq none (setf b (true-list b subst)))))
        (if (null b) a (append a b))
        none)))

(defun member-atom-rewriter (atom subst)
  (mvlet (((:list x l) (args atom)))
    (dereference
     l subst
     :if-constant (if (null l) false none)
     :if-variable none
     :if-compound-appl none
     :if-compound-cons (let ((y (carc l)))
                         (cond
                          ((equal-p x y subst)
                           true)
                          (t
                           (disjoin (make-compound *=* x y)
                                    (make-compound (head atom) x (cdrc l)))))))))

(defun true-list (x &optional subst)
  (dereference
   x subst
   :if-variable none
   :if-compound-appl none
   :if-constant (if (null x) nil none)
   :if-compound-cons (let* ((b (cdr x))
                            (b* (true-list b subst)))
                       (cond
                        ((eq none b*)
                         none)
                        ((eq b b*)
                         x)
                        (t
                         (cons (car x) b*))))))

;;; code-for-lists2.lisp EOF
